g:IMonoid, i, j:. (i+1 = j)  (E:({i..j}|g|). (*,e) i  k < j. E(k) = E(i)) 

latex

Up	groups 1
Definitions of Statement	IMonoid
Definitions	, t  T, P  Q, x:A. B(x), False, A, A  B, P & Q, i  j < k, x. t(x), P  Q, P  Q, x(s), {i..j}, x f y, IMonoid
Lemmas	imon wf, grp car wf, int seg wf, le wf, itop unroll hi, itop unroll base, grp op wf, mon ident